Definition x := nat.
